Definitions | i j, #$n, s ~ t, SQType(T), {T}, SqStable(P), false , true , Dec(P), rps(x;y), Unit, P  Q, x:A B(x), P  Q, T,  b, i< j, True, Prop, Type, , False, P  Q, left+right, x:A. B(x), x:A B(x), t T, if b t else f fi, Case b of inl(x) s(x) ; inr(y) t(y), if a=b c ; d fi, {i..j }, {x:A| B(x) }, i j < k, P & Q, A B, a<b, p  q, p  q, i= j, P Q, A, s = t, , b |